k:, X:(), y, z:( List).
(k  ||y||)
 (k  ||z||)
 (i:{0..k}. y[i] = z[i]  )
 (q-linear(k;j.X(j);y) = q-linear(k;j.X(j);z)  ) 

latex

Definitions	i  j < k, {i..j}, True, T, , P & Q, x. t(x), P  Q, P  Q, , x(s), , i  j , False, A, A  B, P  Q, t  T, x:A. B(x)
Lemmas	qmul wf, q-linear-unroll, true wf, squash wf, qadd wf, q-linear-base, le wf, length wf1, select wf, rationals wf, int seg wf, ge wf, nat properties, nat wf